Nuprl Lemma : R-all-rule2
11,40
postcript
pdf
T
:Type{i},
L
:(
T
List),
R
:({
x
:
T
| (
x
L
)}
es_realizer{i:l}),
P
:({
x
:
T
| (
x
L
)}
event_system{i:l}
prop{i':l}).
(
x
,
y
:
T
. decidable((
x
=
y
)))
l_all(
L
;
T
;
x
.R-realizes{i:l}(
R
(
x
);
es
.
P
(
x
,
es
)))
l_all(
L
;
T
;
x
.l_all(
L
;
T
;
y
.((
(
x
=
y
T
))
R-compat{i:l}(
R
(
x
);
R
(
y
)))))
R-realizes{i:l}
R-realizes
(Rall(
L
;
x
.
R
(
x
));
es
.l_all(
L
;
T
;
x
.
P
(
x
,
es
)))
latex
Definitions
guard(
T
)
,
P
Q
,
x
.
t
(
x
)
,
t
T
,
x
(
s1
,
s2
)
,
x
(
s
)
,
l_all(
L
;
T
;
x
.
P
(
x
))
,
P
Q
,
prop{i:l}
,
x
:
A
.
B
(
x
)
,
decidable(
P
)
Lemmas
es
realizer
wf
,
decidable
wf
,
event
system
wf
,
R-realizes
wf
,
R-compat
wf
,
not
wf
,
l
member
wf
,
R-all-rule
origin